A:Type, P, Q:((A List)Prop).
safety(A;x.P(x))
 (tr1, tr2:A List. tr1  tr2  P(tr2)  Q(tr2)  Q(tr1))
 safety(A;x.P(x) & Q(x)) 

latex

Definitions	{T}, P  Q, x:A. B(x), t  T, Prop, x(s), l1  l2, P & Q, safety(A;tr.P(tr))
Lemmas	iseg wf